#include <stdio.h>

void print_debug(int r4, int r5, int r6, int r7)
{
    cprintf("print_debug: r4=0x%x r5=0x%x r6=0x%x r7=0x%x\n", r4, r5, r6, r7);
}
